/* Empty file for CBMC. */
